$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). ($\forall$$x$:$T$. Dec($P$($x$))) $\Rightarrow$ finite{-}type($T$) $\Rightarrow$ Dec($\exists$$x$:$T$. $P$($x$))